Matches in value-assignements (V): {{numOfValueMatches}}
Matches in edge-description: {{numOfDescriptionMatches}}
Rank |
Scope |
|||
-V- |
{{line.bestrank}}
|
{{line.desc}}
|
| Precondition (initial variable assignment): |
|
{{precondition}} |
| {{fault.rank}}. | {{fault.score}} | Details: | ||||
Current values:
|
||||||
1 | // This file is part of the SV-Benchmarks collection of verification tasks: |
2 | // https://github.com/sosy-lab/sv-benchmarks |
3 | // |
4 | // SPDX-FileCopyrightText: 2010-2020 NIST |
5 | // SPDX-FileCopyrightText: 2020 The SV-Benchmarks Community |
6 | // |
7 | // SPDX-License-Identifier: CC0-1.0 |
8 | |
9 | /* Generated by Frama-C */ |
10 | |
11 | typedef unsigned long size_t; |
12 | |
13 | typedef int wchar_t; |
14 | |
15 | typedef long __int64_t; |
16 | |
17 | typedef __int64_t int64_t; |
18 | |
19 | typedef unsigned int wint_t; |
20 | |
21 | struct _twoIntsStruct { |
22 | int intOne ; |
23 | int intTwo ; |
24 | }; |
25 | |
26 | typedef struct _twoIntsStruct twoIntsStruct; |
27 | |
28 | struct __pthread_internal_list { |
29 | struct __pthread_internal_list *__prev ; |
30 | struct __pthread_internal_list *__next ; |
31 | }; |
32 | |
33 | typedef struct __pthread_internal_list __pthread_list_t; |
34 | |
35 | struct __pthread_mutex_s { |
36 | int __lock ; |
37 | unsigned int __count ; |
38 | int __owner ; |
39 | unsigned int __nusers ; |
40 | int __kind ; |
41 | short __spins ; |
42 | short __elision ; |
43 | __pthread_list_t __list ; |
44 | }; |
45 | |
46 | typedef unsigned long pthread_t; |
47 | |
48 | union __anonunion_pthread_mutexattr_t_36 { |
49 | char __size[4U] ; |
50 | int __align ; |
51 | }; |
52 | |
53 | typedef union __anonunion_pthread_mutexattr_t_36 pthread_mutexattr_t; |
54 | |
55 | union pthread_attr_t { |
56 | char __size[56U] ; |
57 | long __align ; |
58 | }; |
59 | |
60 | typedef union pthread_attr_t pthread_attr_t; |
61 | |
62 | union __anonunion_pthread_mutex_t_38 { |
63 | struct __pthread_mutex_s __data ; |
64 | char __size[40U] ; |
65 | long __align ; |
66 | }; |
67 | |
68 | typedef union __anonunion_pthread_mutex_t_38 pthread_mutex_t; |
69 | |
70 | struct _stdThread; |
71 | |
72 | typedef struct _stdThread *stdThread; |
73 | |
74 | struct _stdThreadLock; |
75 | |
76 | typedef struct _stdThreadLock *stdThreadLock; |
77 | |
78 | struct _stdThread { |
79 | pthread_t handle ; |
80 | void (*start)(void *) ; |
81 | void *args ; |
82 | }; |
83 | |
84 | struct _stdThreadLock { |
85 | pthread_mutex_t mutex ; |
86 | }; |
87 | |
88 | typedef unsigned short __uint16_t; |
89 | |
90 | typedef unsigned int __uint32_t; |
91 | |
92 | typedef long __time_t; |
93 | |
94 | typedef long __ssize_t; |
95 | |
96 | typedef unsigned int __socklen_t; |
97 | |
98 | typedef __ssize_t ssize_t; |
99 | |
100 | typedef __time_t time_t; |
101 | |
102 | typedef __uint16_t uint16_t; |
103 | |
104 | typedef __uint32_t uint32_t; |
105 | |
106 | typedef __socklen_t socklen_t; |
107 | |
108 | typedef unsigned short sa_family_t; |
109 | |
110 | struct sockaddr { |
111 | sa_family_t sa_family ; |
112 | char sa_data[14U] ; |
113 | }; |
114 | |
115 | typedef uint32_t in_addr_t; |
116 | |
117 | struct in_addr { |
118 | in_addr_t s_addr ; |
119 | }; |
120 | |
121 | typedef uint16_t in_port_t; |
122 | |
123 | struct sockaddr_in { |
124 | sa_family_t sin_family ; |
125 | in_port_t sin_port ; |
126 | struct in_addr sin_addr ; |
127 | unsigned char sin_zero[8U] ; |
128 | }; |
129 | |
130 | int printf(char const * , ...); |
131 | |
132 | |
133 | int sscanf(char const *, char const * , ...); |
134 | |
135 | |
136 | int puts(char const *); |
137 | |
138 | |
139 | int rand(void); |
140 | |
141 | |
142 | int iswxdigit(wint_t); |
143 | |
144 | |
145 | unsigned short const **__ctype_b_loc(void); |
146 | |
147 | |
148 | int const GLOBAL_CONST_TRUE; |
149 | |
150 | |
151 | int const GLOBAL_CONST_FALSE; |
152 | |
153 | |
154 | int const GLOBAL_CONST_FIVE; |
155 | |
156 | |
157 | int globalTrue; |
158 | |
159 | |
160 | int globalFalse; |
161 | |
162 | |
163 | int globalFive; |
164 | |
165 | |
166 | void printLine(char const *line); |
167 | |
168 | |
169 | void printWLine(wchar_t const *line); |
170 | |
171 | |
172 | void printIntLine(int intNumber); |
173 | |
174 | |
175 | void printShortLine(short shortNumber); |
176 | |
177 | |
178 | void printFloatLine(float floatNumber); |
179 | |
180 | |
181 | void printLongLine(long longNumber); |
182 | |
183 | |
184 | void printLongLongLine(int64_t longLongIntNumber); |
185 | |
186 | |
187 | void printSizeTLine(size_t sizeTNumber); |
188 | |
189 | |
190 | void printHexCharLine(char charHex); |
191 | |
192 | |
193 | void printWcharLine(wchar_t wideChar); |
194 | |
195 | |
196 | void printUnsignedLine(unsigned int unsignedNumber); |
197 | |
198 | |
199 | void printHexUnsignedCharLine(unsigned char unsignedCharacter); |
200 | |
201 | |
202 | void printDoubleLine(double doubleNumber); |
203 | |
204 | |
205 | void printStructLine(twoIntsStruct const *structTwoIntsStruct); |
206 | |
207 | |
208 | void printBytesLine(unsigned char const *bytes, size_t numBytes); |
209 | |
210 | |
211 | size_t decodeHexChars(unsigned char *bytes, size_t numBytes, char const *hex); |
212 | |
213 | |
214 | size_t decodeHexWChars(unsigned char *bytes, size_t numBytes, wchar_t const *hex); |
215 | |
216 | |
217 | int globalReturnsTrue(void); |
218 | |
219 | |
220 | int globalReturnsFalse(void); |
221 | |
222 | |
223 | int globalReturnsTrueOrFalse(void); |
224 | |
225 | |
226 | int globalArgc; |
227 | |
228 | |
229 | char **globalArgv; |
230 | |
231 | |
232 | int wprintf(wchar_t const * , ...); |
233 | |
234 | |
235 | int swscanf(wchar_t const *, wchar_t const * , ...); |
236 | |
237 | |
238 | void printLine(char const *line) |
239 | { |
240 | |
241 | if (line != (char const *)0) |
242 | printf("%s\n",line); else ; |
243 | |
244 | return; |
245 | } |
246 | |
247 | |
248 | void printWLine(wchar_t const *line) |
249 | { |
250 | |
251 | if (line != (wchar_t const *)0) |
252 | wprintf((wchar_t const *)L"%" "l" "s" "\\n" ,line); else ; |
253 | |
254 | return; |
255 | } |
256 | |
257 | |
258 | void printIntLine(int intNumber) |
259 | { |
260 | |
261 | printf("%d\n",intNumber); |
262 | |
263 | return; |
264 | } |
265 | |
266 | |
267 | |
268 | |
269 | void printFloatLine(float floatNumber) |
270 | { |
271 | |
272 | printf("%f\n",(double)floatNumber); |
273 | |
274 | return; |
275 | } |
276 | |
277 | |
278 | void printLongLine(long longNumber) |
279 | { |
280 | |
281 | printf("%ld\n",longNumber); |
282 | |
283 | return; |
284 | } |
285 | |
286 | |
287 | |
288 | |
289 | void printSizeTLine(size_t sizeTNumber) |
290 | { |
291 | |
292 | printf("%zu\n",sizeTNumber); |
293 | |
294 | return; |
295 | } |
296 | |
297 | |
298 | void printHexCharLine(char charHex) |
299 | { |
300 | |
301 | printf("%02x\n",(int)charHex); |
302 | |
303 | return; |
304 | } |
305 | |
306 | |
307 | void printWcharLine(wchar_t wideChar) |
308 | { |
309 | wchar_t s[2U]; |
310 | |
311 | s[0] = wideChar; |
312 | |
313 | s[1] = 0; |
314 | |
315 | printf("%ls\n",(wchar_t *)(& s)); |
316 | |
317 | return; |
318 | } |
319 | |
320 | |
321 | void printUnsignedLine(unsigned int unsignedNumber) |
322 | { |
323 | |
324 | printf("%u\n",unsignedNumber); |
325 | |
326 | return; |
327 | } |
328 | |
329 | |
330 | void printHexUnsignedCharLine(unsigned char unsignedCharacter) |
331 | { |
332 | |
333 | printf("%02x\n",(int)unsignedCharacter); |
334 | |
335 | return; |
336 | } |
337 | |
338 | |
339 | void printDoubleLine(double doubleNumber) |
340 | { |
341 | |
342 | printf("%g\n",doubleNumber); |
343 | |
344 | return; |
345 | } |
346 | |
347 | |
348 | void printStructLine(twoIntsStruct const *structTwoIntsStruct) |
349 | { |
350 | |
351 | printf("%d -- %d\n",structTwoIntsStruct->intOne,structTwoIntsStruct->intTwo); |
352 | |
353 | return; |
354 | } |
355 | |
356 | |
357 | void printBytesLine(unsigned char const *bytes, size_t numBytes) |
358 | { |
359 | size_t i; |
360 | |
361 | i = 0UL; |
362 | |
363 | goto ldv_3392; |
364 | ldv_3391: |
365 | ; |
366 | |
367 | printf("%02x",(int)*(bytes + i)); |
368 | |
369 | i += 1UL; |
370 | ldv_3392: |
371 | ; |
372 | |
373 | if (i < numBytes) |
374 | goto ldv_3391; else |
375 | goto ldv_3393; |
376 | ldv_3393: |
377 | ; |
378 | |
379 | puts(""); |
380 | |
381 | return; |
382 | } |
383 | |
384 | |
385 | size_t decodeHexChars(unsigned char *bytes, size_t numBytes, char const *hex) |
386 | { |
387 | |
388 | size_t numWritten = 0UL; |
389 | |
390 | goto ldv_3402; |
391 | ldv_3401: |
392 | ; |
393 | { |
394 | int byte; |
395 | |
396 | sscanf(hex + numWritten * 2UL,"%02x",& byte); |
397 | |
398 | *(bytes + numWritten) = (unsigned char)byte; |
399 | |
400 | numWritten += 1UL; |
401 | } |
402 | ldv_3402: |
403 | ; |
404 | |
405 | if (numWritten < numBytes) { |
406 | unsigned short const **tmp; |
407 | |
408 | tmp = __ctype_b_loc(); |
409 | |
410 | ; |
411 | |
412 | if (((int)*(*tmp + (int)*(hex + numWritten * 2UL)) & 4096) != 0) { |
413 | unsigned short const **tmp_0; |
414 | |
415 | tmp_0 = __ctype_b_loc(); |
416 | |
417 | ; |
418 | |
419 | if (((int)*(*tmp_0 + (int)*(hex + (numWritten * 2UL + (size_t)1U))) & 4096) != 0) |
420 | |
421 | goto ldv_3401; else |
422 | goto ldv_3403; |
423 | } |
424 | else |
425 | goto ldv_3403; |
426 | } |
427 | else |
428 | goto ldv_3403; |
429 | ldv_3403: |
430 | ; |
431 | |
432 | return numWritten; |
433 | } |
434 | |
435 | |
436 | size_t decodeHexWChars(unsigned char *bytes, size_t numBytes, wchar_t const *hex) |
437 | { |
438 | |
439 | size_t numWritten = 0UL; |
440 | |
441 | goto ldv_3412; |
442 | ldv_3411: |
443 | ; |
444 | { |
445 | int byte; |
446 | |
447 | swscanf(hex + numWritten * 2UL,(wchar_t const *)L"%" "0" "2" "x" ,& byte); |
448 | |
449 | *(bytes + numWritten) = (unsigned char)byte; |
450 | |
451 | numWritten += 1UL; |
452 | } |
453 | ldv_3412: |
454 | ; |
455 | |
456 | if (numWritten < numBytes) { |
457 | int tmp; |
458 | |
459 | tmp = iswxdigit((unsigned int)*(hex + numWritten * 2UL)); |
460 | |
461 | if (tmp != 0) { |
462 | int tmp_0; |
463 | |
464 | tmp_0 = iswxdigit((unsigned int)*(hex + (numWritten * 2UL + (size_t)1U))); |
465 | |
466 | if (tmp_0 != 0) |
467 | goto ldv_3411; else |
468 | goto ldv_3413; |
469 | } |
470 | else |
471 | goto ldv_3413; |
472 | } |
473 | else |
474 | goto ldv_3413; |
475 | ldv_3413: |
476 | ; |
477 | |
478 | return numWritten; |
479 | } |
480 | |
481 | |
482 | int globalReturnsTrue(void) |
483 | { |
484 | int __retres; |
485 | |
486 | __retres = 1; |
487 | |
488 | return __retres; |
489 | } |
490 | |
491 | |
492 | int globalReturnsFalse(void) |
493 | { |
494 | int __retres; |
495 | |
496 | __retres = 0; |
497 | |
498 | return __retres; |
499 | } |
500 | |
501 | |
502 | int globalReturnsTrueOrFalse(void) |
503 | { |
504 | int __retres; |
505 | int tmp; |
506 | |
507 | tmp = rand(); |
508 | |
509 | __retres = tmp % 2; |
510 | |
511 | return __retres; |
512 | } |
513 | |
514 | |
515 | int const GLOBAL_CONST_TRUE = 1; |
516 | |
517 | int const GLOBAL_CONST_FALSE = 0; |
518 | |
519 | int const GLOBAL_CONST_FIVE = 5; |
520 | |
521 | int globalTrue = 1; |
522 | |
523 | int globalFalse = 0; |
524 | |
525 | int globalFive = 5; |
526 | |
527 | void good1(void) |
528 | { |
529 | |
530 | return; |
531 | } |
532 | |
533 | |
534 | void good2(void) |
535 | { |
536 | |
537 | return; |
538 | } |
539 | |
540 | |
541 | void good3(void) |
542 | { |
543 | |
544 | return; |
545 | } |
546 | |
547 | |
548 | void good4(void) |
549 | { |
550 | |
551 | return; |
552 | } |
553 | |
554 | |
555 | void good5(void) |
556 | { |
557 | |
558 | return; |
559 | } |
560 | |
561 | |
562 | void good6(void) |
563 | { |
564 | |
565 | return; |
566 | } |
567 | |
568 | |
569 | void good7(void) |
570 | { |
571 | |
572 | return; |
573 | } |
574 | |
575 | |
576 | void good8(void) |
577 | { |
578 | |
579 | return; |
580 | } |
581 | |
582 | |
583 | void good9(void) |
584 | { |
585 | |
586 | return; |
587 | } |
588 | |
589 | |
590 | void bad1(void) |
591 | { |
592 | |
593 | return; |
594 | } |
595 | |
596 | |
597 | void bad2(void) |
598 | { |
599 | |
600 | return; |
601 | } |
602 | |
603 | |
604 | void bad3(void) |
605 | { |
606 | |
607 | return; |
608 | } |
609 | |
610 | |
611 | void bad4(void) |
612 | { |
613 | |
614 | return; |
615 | } |
616 | |
617 | |
618 | void bad5(void) |
619 | { |
620 | |
621 | return; |
622 | } |
623 | |
624 | |
625 | void bad6(void) |
626 | { |
627 | |
628 | return; |
629 | } |
630 | |
631 | |
632 | void bad7(void) |
633 | { |
634 | |
635 | return; |
636 | } |
637 | |
638 | |
639 | void bad8(void) |
640 | { |
641 | |
642 | return; |
643 | } |
644 | |
645 | |
646 | void bad9(void) |
647 | { |
648 | |
649 | return; |
650 | } |
651 | |
652 | |
653 | int globalArgc = 0; |
654 | |
655 | char **globalArgv = (char **)0; |
656 | |
657 | void *malloc(size_t); |
658 | |
659 | |
660 | void free(void *); |
661 | |
662 | |
663 | int pthread_create(pthread_t *, pthread_attr_t const *, void *(*)(void *), void *); |
664 | |
665 | |
666 | void pthread_exit(void *); |
667 | |
668 | |
669 | int pthread_join(pthread_t, void **); |
670 | |
671 | |
672 | int pthread_mutex_init(pthread_mutex_t *, pthread_mutexattr_t const *); |
673 | |
674 | |
675 | int pthread_mutex_destroy(pthread_mutex_t *); |
676 | |
677 | |
678 | int pthread_mutex_lock(pthread_mutex_t *); |
679 | |
680 | |
681 | int pthread_mutex_unlock(pthread_mutex_t *); |
682 | |
683 | |
684 | int stdThreadCreate(void (*start)(void *), void *args, stdThread *thread); |
685 | |
686 | |
687 | int stdThreadJoin(stdThread thread); |
688 | |
689 | |
690 | int stdThreadDestroy(stdThread thread); |
691 | |
692 | |
693 | int stdThreadLockCreate(stdThreadLock *lock); |
694 | |
695 | |
696 | void stdThreadLockAcquire(stdThreadLock lock); |
697 | |
698 | |
699 | void stdThreadLockRelease(stdThreadLock lock); |
700 | |
701 | |
702 | void stdThreadLockDestroy(stdThreadLock lock); |
703 | |
704 | |
705 | static void *internal_start(void *args) |
706 | { |
707 | void *__retres; |
708 | |
709 | stdThread thread = (struct _stdThread *)args; |
710 | |
711 | (*(thread->start))(thread->args); |
712 | |
713 | pthread_exit((void *)0); |
714 | |
715 | __retres = (void *)0; |
716 | |
717 | return __retres; |
718 | } |
719 | |
720 | |
721 | int stdThreadCreate(void (*start)(void *), void *args, stdThread *thread) |
722 | { |
723 | int __retres; |
724 | pthread_t handle; |
725 | stdThread my_thread; |
726 | int tmp_0; |
727 | |
728 | *thread = (struct _stdThread *)0; |
729 | |
730 | my_thread = (stdThread)malloc(24UL); |
731 | |
732 | if (my_thread == (struct _stdThread *)0) { |
733 | |
734 | __retres = 0; |
735 | |
736 | goto return_label; |
737 | } |
738 | else ; |
739 | |
740 | my_thread->start = start; |
741 | |
742 | my_thread->args = args; |
743 | |
744 | tmp_0 = pthread_create(& handle,(pthread_attr_t const *)0,& internal_start,(void *)my_thread); |
745 | |
746 | if (tmp_0 != 0) { |
747 | |
748 | free((void *)my_thread); |
749 | |
750 | __retres = 0; |
751 | |
752 | goto return_label; |
753 | } |
754 | else ; |
755 | |
756 | my_thread->handle = handle; |
757 | |
758 | *thread = my_thread; |
759 | |
760 | __retres = 1; |
761 | return_label: |
762 | return __retres; |
763 | } |
764 | |
765 | |
766 | int stdThreadJoin(stdThread thread) |
767 | { |
768 | int __retres; |
769 | void *dummy; |
770 | int tmp; |
771 | |
772 | tmp = pthread_join(thread->handle,& dummy); |
773 | |
774 | if (tmp != 0) { |
775 | |
776 | __retres = 0; |
777 | |
778 | goto return_label; |
779 | } |
780 | else ; |
781 | |
782 | __retres = 1; |
783 | return_label: |
784 | return __retres; |
785 | } |
786 | |
787 | |
788 | int stdThreadDestroy(stdThread thread) |
789 | { |
790 | int __retres; |
791 | |
792 | free((void *)thread); |
793 | |
794 | __retres = 1; |
795 | |
796 | return __retres; |
797 | } |
798 | |
799 | |
800 | int stdThreadLockCreate(stdThreadLock *lock) |
801 | { |
802 | int __retres; |
803 | int tmp_0; |
804 | |
805 | stdThreadLock my_lock = (struct _stdThreadLock *)0; |
806 | |
807 | *lock = (struct _stdThreadLock *)0; |
808 | |
809 | my_lock = (stdThreadLock)malloc(40UL); |
810 | |
811 | if (my_lock == (struct _stdThreadLock *)0) { |
812 | |
813 | __retres = 0; |
814 | |
815 | goto return_label; |
816 | } |
817 | else ; |
818 | |
819 | tmp_0 = pthread_mutex_init(& my_lock->mutex,(pthread_mutexattr_t const *)0); |
820 | |
821 | if (tmp_0 != 0) { |
822 | |
823 | free((void *)lock); |
824 | |
825 | __retres = 0; |
826 | |
827 | goto return_label; |
828 | } |
829 | else ; |
830 | |
831 | *lock = my_lock; |
832 | |
833 | __retres = 1; |
834 | return_label: |
835 | return __retres; |
836 | } |
837 | |
838 | |
839 | void stdThreadLockAcquire(stdThreadLock lock) |
840 | { |
841 | |
842 | pthread_mutex_lock(& lock->mutex); |
843 | |
844 | return; |
845 | } |
846 | |
847 | |
848 | void stdThreadLockRelease(stdThreadLock lock) |
849 | { |
850 | |
851 | pthread_mutex_unlock(& lock->mutex); |
852 | |
853 | return; |
854 | } |
855 | |
856 | |
857 | void stdThreadLockDestroy(stdThreadLock lock) |
858 | { |
859 | |
860 | pthread_mutex_destroy(& lock->mutex); |
861 | |
862 | free((void *)lock); |
863 | |
864 | return; |
865 | } |
866 | |
867 | |
868 | void ldv_exit(void); |
869 | |
870 | |
871 | char *ldv_strcpy(char *dest, char const *src); |
872 | |
873 | |
874 | size_t ldv_strlen(char const *str); |
875 | |
876 | |
877 | unsigned long strtoul(char const *, char **, int); |
878 | |
879 | |
880 | void srand(unsigned int); |
881 | |
882 | |
883 | static void ldv_exit_2(int ldv_func_arg1); |
884 | |
885 | |
886 | time_t time(time_t *); |
887 | |
888 | |
889 | void *memset(void *, int, size_t); |
890 | |
891 | |
892 | static char *ldv_strcpy_3(char * __restrict ldv_func_arg1, char const * __restrict ldv_func_arg2); |
893 | |
894 | |
895 | static size_t ldv_strlen_1(char const *ldv_func_arg1); |
896 | |
897 | |
898 | int socket(int, int, int); |
899 | |
900 | |
901 | int connect(int, struct sockaddr const *, socklen_t); |
902 | |
903 | |
904 | ssize_t recv(int, void *, size_t, int); |
905 | |
906 | |
907 | uint16_t htons(uint16_t); |
908 | |
909 | |
910 | in_addr_t inet_addr(char const *); |
911 | |
912 | |
913 | int close(int); |
914 | |
915 | |
916 | void CWE789_Uncontrolled_Mem_Alloc__malloc_char_connect_socket_01_bad(void) |
917 | { |
918 | size_t data; |
919 | |
920 | data = 0UL; |
921 | { |
922 | int recvResult; |
923 | struct sockaddr_in service; |
924 | char inputBuffer[26U]; |
925 | int tmp; |
926 | ssize_t tmp_0; |
927 | |
928 | int connectSocket = -1; |
929 | |
930 | connectSocket = socket(2,1,6); |
931 | |
932 | if (connectSocket == -1) |
933 | goto ldv_4160; else ; |
934 | |
935 | memset((void *)(& service),0,16UL); |
936 | |
937 | service.sin_family = (unsigned short)2U; |
938 | |
939 | service.sin_addr.s_addr = inet_addr("127.0.0.1"); |
940 | |
941 | service.sin_port = htons((unsigned short)27015); |
942 | |
943 | tmp = connect(connectSocket,(struct sockaddr const *)(& service),16U); |
944 | |
945 | if (tmp == -1) |
946 | goto ldv_4160; else ; |
947 | |
948 | tmp_0 = recv(connectSocket,(void *)(& inputBuffer),25UL,0); |
949 | |
950 | recvResult = (int)tmp_0; |
951 | |
952 | if (recvResult == -1 || recvResult == 0) |
953 | goto ldv_4160; else ; |
954 | |
955 | inputBuffer[recvResult] = (char)0; |
956 | |
957 | data = strtoul((char const *)(& inputBuffer),(char **)0,0); |
958 | ldv_4160: |
959 | ; |
960 | |
961 | if (connectSocket != -1) |
962 | close(connectSocket); else ; |
963 | } |
964 | { |
965 | char *myString; |
966 | size_t tmp_2; |
967 | |
968 | tmp_2 = ldv_strlen_1("hello"); |
969 | |
970 | ; |
971 | |
972 | if (tmp_2 < data) { |
973 | |
974 | myString = (char *)malloc(data); |
975 | |
976 | if (myString == (char *)0) |
977 | ldv_exit_2(-1); else ; |
978 | |
979 | ldv_strcpy_3(myString,"hello"); |
980 | |
981 | printLine((char const *)myString); |
982 | |
983 | free((void *)myString); |
984 | } |
985 | else |
986 | printLine("Input is less than the length of the source string"); |
987 | } |
988 | |
989 | return; |
990 | } |
991 | |
992 | |
993 | int main(int argc, char **argv) |
994 | { |
995 | int __retres; |
996 | { |
997 | time_t tmp; |
998 | |
999 | tmp = time((time_t *)0L); |
1000 | |
1001 | srand((unsigned int)tmp); |
1002 | |
1003 | printLine("Calling bad()..."); |
1004 | |
1005 | CWE789_Uncontrolled_Mem_Alloc__malloc_char_connect_socket_01_bad(); |
1006 | |
1007 | printLine("Finished bad()"); |
1008 | |
1009 | __retres = 0; |
1010 | |
1011 | goto return_label; |
1012 | } |
1013 | |
1014 | __retres = 0; |
1015 | return_label: |
1016 | return __retres; |
1017 | } |
1018 | |
1019 | |
1020 | static size_t ldv_strlen_1(char const *ldv_func_arg1) |
1021 | { |
1022 | size_t tmp; |
1023 | |
1024 | tmp = ldv_strlen(ldv_func_arg1); |
1025 | |
1026 | return tmp; |
1027 | } |
1028 | |
1029 | |
1030 | static void ldv_exit_2(int ldv_func_arg1) |
1031 | { |
1032 | |
1033 | ldv_exit(); |
1034 | |
1035 | return; |
1036 | } |
1037 | |
1038 | |
1039 | static char *ldv_strcpy_3(char * __restrict ldv_func_arg1, char const * __restrict ldv_func_arg2) |
1040 | { |
1041 | char *tmp; |
1042 | |
1043 | tmp = ldv_strcpy(ldv_func_arg1,ldv_func_arg2); |
1044 | |
1045 | return tmp; |
1046 | } |
1047 | |
1048 | |
1049 | void *ldv_xmalloc(size_t size); |
1050 | |
1051 | |
1052 | int ldv_undef_int(void); |
1053 | |
1054 | |
1055 | int ldv_undef_int_positive(void); |
1056 | |
1057 | |
1058 | int ldv_asprintf(char **ptr); |
1059 | |
1060 | |
1061 | int ldv_asprintf(char **ptr) |
1062 | { |
1063 | int __retres; |
1064 | char *new; |
1065 | int tmp_1; |
1066 | |
1067 | tmp_1 = ldv_undef_int(); |
1068 | |
1069 | if (tmp_1 != 0) { |
1070 | int tmp_0; |
1071 | |
1072 | new = (char *)ldv_xmalloc(1UL); |
1073 | |
1074 | *ptr = new; |
1075 | |
1076 | tmp_0 = ldv_undef_int_positive(); |
1077 | |
1078 | __retres = tmp_0; |
1079 | |
1080 | goto return_label; |
1081 | } |
1082 | else { |
1083 | |
1084 | __retres = -1; |
1085 | |
1086 | goto return_label; |
1087 | } |
1088 | return_label: |
1089 | return __retres; |
1090 | } |
1091 | |
1092 | |
1093 | void abort(void); |
1094 | void assume_abort_if_not(int cond) { |
1095 | if(!cond) {abort();} |
1096 | } |
1097 | |
1098 | |
1099 | void ldv_exit(void) |
1100 | { |
1101 | |
1102 | assume_abort_if_not(0); |
1103 | |
1104 | return; |
1105 | } |
1106 | |
1107 | |
1108 | void *ldv_xmalloc(size_t size); |
1109 | |
1110 | |
1111 | void *memcpy(void *, void const *, size_t); |
1112 | |
1113 | |
1114 | char *ldv_strdup(char const *s); |
1115 | |
1116 | |
1117 | char *ldv_strncpy(char *dest, char const *src, size_t n); |
1118 | |
1119 | |
1120 | char *ldv_strdup(char const *s) |
1121 | { |
1122 | char *__retres; |
1123 | char *new; |
1124 | int tmp_2; |
1125 | |
1126 | tmp_2 = ldv_undef_int(); |
1127 | |
1128 | if (tmp_2 != 0) { |
1129 | void *tmp_0; |
1130 | size_t tmp; |
1131 | size_t tmp_1; |
1132 | |
1133 | tmp = ldv_strlen(s); |
1134 | |
1135 | tmp_0 = ldv_xmalloc(tmp); |
1136 | |
1137 | new = (char *)tmp_0; |
1138 | |
1139 | tmp_1 = ldv_strlen(s); |
1140 | |
1141 | ; |
1142 | |
1143 | ; |
1144 | |
1145 | memcpy((void *)new,(void const *)s,tmp_1); |
1146 | |
1147 | __retres = new; |
1148 | |
1149 | goto return_label; |
1150 | } |
1151 | else { |
1152 | |
1153 | __retres = (char *)0; |
1154 | |
1155 | goto return_label; |
1156 | } |
1157 | return_label: |
1158 | return __retres; |
1159 | } |
1160 | |
1161 | |
1162 | size_t ldv_strlen(char const *str) |
1163 | { |
1164 | size_t __retres; |
1165 | char const *s; |
1166 | |
1167 | s = str; |
1168 | |
1169 | goto ldv_1424; |
1170 | ldv_1423: |
1171 | ; |
1172 | |
1173 | s += 1; |
1174 | ldv_1424: |
1175 | ; |
1176 | |
1177 | if ((int)*s != 0) |
1178 | goto ldv_1423; else |
1179 | goto ldv_1425; |
1180 | ldv_1425: |
1181 | ; |
1182 | |
1183 | __retres = (unsigned long)((long)s - (long)str); |
1184 | |
1185 | return __retres; |
1186 | } |
1187 | |
1188 | |
1189 | char *ldv_strncpy(char *dest, char const *src, size_t n) |
1190 | { |
1191 | size_t i; |
1192 | |
1193 | i = 0UL; |
1194 | |
1195 | goto ldv_1433; |
1196 | ldv_1432: |
1197 | ; |
1198 | |
1199 | *(dest + i) = *(src + i); |
1200 | |
1201 | i += 1UL; |
1202 | ldv_1433: |
1203 | ; |
1204 | |
1205 | if (i < n && (int)*(src + i) != 0) |
1206 | goto ldv_1432; else |
1207 | goto ldv_1434; |
1208 | ldv_1434: |
1209 | ; |
1210 | |
1211 | goto ldv_1436; |
1212 | ldv_1435: |
1213 | ; |
1214 | |
1215 | *(dest + i) = (char)0; |
1216 | |
1217 | i += 1UL; |
1218 | ldv_1436: |
1219 | ; |
1220 | |
1221 | if (i < n) |
1222 | goto ldv_1435; else |
1223 | goto ldv_1437; |
1224 | ldv_1437: |
1225 | ; |
1226 | |
1227 | return dest; |
1228 | } |
1229 | |
1230 | |
1231 | char *ldv_strcpy(char *dest, char const *src) |
1232 | { |
1233 | size_t tmp; |
1234 | |
1235 | tmp = ldv_strlen(src); |
1236 | |
1237 | ; |
1238 | |
1239 | ; |
1240 | |
1241 | memcpy((void *)dest,(void const *)src,tmp); |
1242 | |
1243 | return dest; |
1244 | } |
1245 | |
1246 | |
1247 | void *ldv_malloc(size_t size); |
1248 | |
1249 | |
1250 | void *ldv_calloc(size_t nmemb, size_t size); |
1251 | |
1252 | |
1253 | void *ldv_zalloc(size_t size); |
1254 | |
1255 | |
1256 | void ldv_free(void *s); |
1257 | |
1258 | |
1259 | void *ldv_realloc(void *ptr, size_t size); |
1260 | |
1261 | |
1262 | void *ldv_xzalloc(size_t size); |
1263 | |
1264 | |
1265 | |
1266 | |
1267 | |
1268 | |
1269 | |
1270 | |
1271 | void *ldv_reference_malloc(size_t size); |
1272 | |
1273 | |
1274 | void *ldv_reference_calloc(size_t nmemb, size_t size); |
1275 | |
1276 | |
1277 | void *ldv_reference_zalloc(size_t size); |
1278 | |
1279 | |
1280 | void ldv_reference_free(void *s); |
1281 | |
1282 | |
1283 | void *ldv_reference_realloc(void *ptr, size_t size); |
1284 | |
1285 | |
1286 | void *ldv_reference_xmalloc(size_t size); |
1287 | |
1288 | |
1289 | void *ldv_reference_xzalloc(size_t size); |
1290 | |
1291 | |
1292 | |
1293 | |
1294 | |
1295 | |
1296 | |
1297 | |
1298 | |
1299 | |
1300 | void *ldv_malloc(size_t size) |
1301 | { |
1302 | void *tmp; |
1303 | |
1304 | tmp = ldv_reference_malloc(size); |
1305 | |
1306 | return tmp; |
1307 | } |
1308 | |
1309 | |
1310 | void *ldv_calloc(size_t nmemb, size_t size) |
1311 | { |
1312 | void *tmp; |
1313 | |
1314 | tmp = ldv_reference_calloc(nmemb,size); |
1315 | |
1316 | return tmp; |
1317 | } |
1318 | |
1319 | |
1320 | void *ldv_zalloc(size_t size) |
1321 | { |
1322 | void *tmp; |
1323 | |
1324 | tmp = ldv_reference_zalloc(size); |
1325 | |
1326 | return tmp; |
1327 | } |
1328 | |
1329 | |
1330 | void ldv_free(void *s) |
1331 | { |
1332 | |
1333 | ldv_reference_free(s); |
1334 | |
1335 | return; |
1336 | } |
1337 | |
1338 | |
1339 | void *ldv_xmalloc(size_t size) |
1340 | { |
1341 | void *tmp; |
1342 | |
1343 | tmp = ldv_reference_xmalloc(size); |
1344 | |
1345 | return tmp; |
1346 | } |
1347 | |
1348 | |
1349 | void *ldv_xzalloc(size_t size) |
1350 | { |
1351 | void *tmp; |
1352 | |
1353 | tmp = ldv_reference_xzalloc(size); |
1354 | |
1355 | return tmp; |
1356 | } |
1357 | |
1358 | |
1359 | |
1360 | |
1361 | |
1362 | |
1363 | |
1364 | |
1365 | |
1366 | |
1367 | void *ldv_realloc(void *ptr, size_t size) |
1368 | { |
1369 | void *tmp; |
1370 | |
1371 | tmp = ldv_reference_realloc(ptr,size); |
1372 | |
1373 | return tmp; |
1374 | } |
1375 | |
1376 | |
1377 | void abort(void); |
1378 | extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__)); |
1379 | void reach_error() { __assert_fail("0", "CWE789_Uncontrolled_Mem_Alloc---s01---CWE789_Uncontrolled_Mem_Alloc__malloc_char_connect_socket_01_bad.i", 1371, "reach_error"); } |
1380 | |
1381 | |
1382 | void ldv_error(void); |
1383 | |
1384 | |
1385 | void ldv_error(void) |
1386 | { |
1387 | |
1388 | {reach_error();} |
1389 | |
1390 | return; |
1391 | } |
1392 | |
1393 | |
1394 | |
1395 | |
1396 | |
1397 | int ldv_undef_long(void); |
1398 | |
1399 | |
1400 | unsigned int ldv_undef_uint(void); |
1401 | |
1402 | |
1403 | unsigned long ldv_undef_ulong(void); |
1404 | |
1405 | |
1406 | unsigned long long ldv_undef_ulonglong(void); |
1407 | |
1408 | |
1409 | |
1410 | |
1411 | int ldv_undef_int_negative(void); |
1412 | |
1413 | |
1414 | int ldv_undef_int_nonpositive(void); |
1415 | |
1416 | |
1417 | |
1418 | |
1419 | int __VERIFIER_nondet_int(void); |
1420 | |
1421 | |
1422 | long __VERIFIER_nondet_long(void); |
1423 | |
1424 | |
1425 | unsigned int __VERIFIER_nondet_uint(void); |
1426 | |
1427 | |
1428 | unsigned long __VERIFIER_nondet_ulong(void); |
1429 | |
1430 | |
1431 | unsigned long long __VERIFIER_nondet_ulonglong(void); |
1432 | |
1433 | |
1434 | |
1435 | |
1436 | int ldv_undef_int(void) |
1437 | { |
1438 | int tmp; |
1439 | |
1440 | tmp = __VERIFIER_nondet_int(); |
1441 | |
1442 | return tmp; |
1443 | } |
1444 | |
1445 | |
1446 | int ldv_undef_long(void) |
1447 | { |
1448 | int __retres; |
1449 | long tmp; |
1450 | |
1451 | tmp = __VERIFIER_nondet_long(); |
1452 | |
1453 | __retres = (int)tmp; |
1454 | |
1455 | return __retres; |
1456 | } |
1457 | |
1458 | |
1459 | unsigned int ldv_undef_uint(void) |
1460 | { |
1461 | unsigned int tmp; |
1462 | |
1463 | tmp = __VERIFIER_nondet_uint(); |
1464 | |
1465 | return tmp; |
1466 | } |
1467 | |
1468 | |
1469 | |
1470 | |
1471 | unsigned long ldv_undef_ulong(void) |
1472 | { |
1473 | unsigned long tmp; |
1474 | |
1475 | tmp = __VERIFIER_nondet_ulong(); |
1476 | |
1477 | return tmp; |
1478 | } |
1479 | |
1480 | |
1481 | unsigned long long ldv_undef_ulonglong(void) |
1482 | { |
1483 | unsigned long long tmp; |
1484 | |
1485 | tmp = __VERIFIER_nondet_ulonglong(); |
1486 | |
1487 | return tmp; |
1488 | } |
1489 | |
1490 | |
1491 | int ldv_undef_int_positive(void) |
1492 | { |
1493 | |
1494 | int ret = ldv_undef_int(); |
1495 | |
1496 | assume_abort_if_not(ret > 0); |
1497 | |
1498 | return ret; |
1499 | } |
1500 | |
1501 | |
1502 | int ldv_undef_int_negative(void) |
1503 | { |
1504 | |
1505 | int ret = ldv_undef_int(); |
1506 | |
1507 | assume_abort_if_not(ret < 0); |
1508 | |
1509 | return ret; |
1510 | } |
1511 | |
1512 | |
1513 | int ldv_undef_int_nonpositive(void) |
1514 | { |
1515 | |
1516 | int ret = ldv_undef_int(); |
1517 | |
1518 | assume_abort_if_not(ret <= 0); |
1519 | |
1520 | return ret; |
1521 | } |
1522 | |
1523 | |
1524 | |
1525 | |
1526 | |
1527 | |
1528 | void *calloc(size_t, size_t); |
1529 | |
1530 | |
1531 | void *ldv_reference_malloc(size_t size) |
1532 | { |
1533 | void *__retres; |
1534 | void *res; |
1535 | int tmp; |
1536 | |
1537 | tmp = ldv_undef_int(); |
1538 | |
1539 | if (tmp != 0) { |
1540 | |
1541 | res = malloc(size); |
1542 | |
1543 | assume_abort_if_not(res != (void *)0); |
1544 | |
1545 | __retres = res; |
1546 | |
1547 | goto return_label; |
1548 | } |
1549 | else { |
1550 | |
1551 | __retres = (void *)0; |
1552 | |
1553 | goto return_label; |
1554 | } |
1555 | return_label: |
1556 | return __retres; |
1557 | } |
1558 | |
1559 | |
1560 | void *ldv_reference_calloc(size_t nmemb, size_t size) |
1561 | { |
1562 | void *tmp; |
1563 | |
1564 | tmp = calloc(nmemb,size); |
1565 | |
1566 | return tmp; |
1567 | } |
1568 | |
1569 | |
1570 | void *ldv_reference_zalloc(size_t size) |
1571 | { |
1572 | void *tmp; |
1573 | |
1574 | tmp = calloc(1UL,size); |
1575 | |
1576 | return tmp; |
1577 | } |
1578 | |
1579 | |
1580 | void ldv_reference_free(void *s) |
1581 | { |
1582 | |
1583 | free(s); |
1584 | |
1585 | return; |
1586 | } |
1587 | |
1588 | |
1589 | void *ldv_reference_realloc(void *ptr, size_t size) |
1590 | { |
1591 | void *__retres; |
1592 | void *res; |
1593 | int tmp; |
1594 | |
1595 | if (ptr != (void *)0 && size == 0UL) { |
1596 | |
1597 | free(ptr); |
1598 | |
1599 | __retres = (void *)0; |
1600 | |
1601 | goto return_label; |
1602 | } |
1603 | else ; |
1604 | |
1605 | if (ptr == (void *)0) { |
1606 | |
1607 | res = malloc(size); |
1608 | |
1609 | __retres = res; |
1610 | |
1611 | goto return_label; |
1612 | } |
1613 | else ; |
1614 | |
1615 | tmp = ldv_undef_int(); |
1616 | |
1617 | if (tmp != 0) { |
1618 | |
1619 | res = malloc(size); |
1620 | |
1621 | assume_abort_if_not(res != (void *)0); |
1622 | |
1623 | memcpy(res,(void const *)ptr,size); |
1624 | |
1625 | free(ptr); |
1626 | |
1627 | __retres = res; |
1628 | |
1629 | goto return_label; |
1630 | } |
1631 | else { |
1632 | |
1633 | __retres = (void *)0; |
1634 | |
1635 | goto return_label; |
1636 | } |
1637 | return_label: |
1638 | return __retres; |
1639 | } |
1640 | |
1641 | |
1642 | void *ldv_reference_xmalloc(size_t size) |
1643 | { |
1644 | void *res; |
1645 | |
1646 | res = malloc(size); |
1647 | |
1648 | assume_abort_if_not(res != (void *)0); |
1649 | |
1650 | return res; |
1651 | } |
1652 | |
1653 | |
1654 | void *ldv_reference_xzalloc(size_t size) |
1655 | { |
1656 | void *res; |
1657 | |
1658 | res = calloc(1UL,size); |
1659 | |
1660 | assume_abort_if_not(res != (void *)0); |
1661 | |
1662 | return res; |
1663 | } |
1664 | |
1665 | |
1666 | |
1667 | |
1668 | |
1669 | |
1670 | |
1671 | |
1672 | |
1673 |
Log not available
| Statistics Name | Statistics Value | Additional Value |
|---|---|---|
| Parallel Algorithm statistics | ||
| Number of algorithms used | 5 | |
| Successful analysis | /opt/cpachecker/config/components/smgAnalysis-symEx.properties | |
| Statistics for | /opt/cpachecker/config/components/smgAnalysis-symEx.properties | |
| ============================================================================== | ||
| SMGCPA statistics | ||
| Number of variables per state | 17.51 | sum: 613, count: 35, min: 0, max: 25 |
| Number of global variables per state | 8.51 | sum: 298, count: 35, min: 0, max: 10 |
| Time for solving constraints | 0.361s | |
| Time for independent computation | 0.010s | |
| Time for SMT check | 0.007s | |
| Time for resolving definites | 0.028s | |
| Cache lookups | 13 | |
| Direct cache hits | 3 | |
| Direct cache lookup time | 0.001s | |
| Number of assumptions | 20 | |
| Number of deterministic assumptions | 0 | |
| Level of Determinism | 0% | |
| Number of list materializations | : 0 | |
| Total time spent on materialization | : 0ms | |
| Max time spent on materialization | : 0ms | |
| Number of 0+ materializations | 0 | |
| Total time spent on 0+ materialization | : 0ms | |
| Max time spent on 0+ materialization | : 0ms | |
| Number of lists abstracted in total | : 0 | |
| Total time spent on list abstraction | : 0ms | |
| Max time spent on list abstraction | : 0ms | |
| Total time spent on searching for list abstractions | : 0ms | |
| Max time spent on searching a single list abstractions | : 0ms | |
| AutomatonAnalysis (SMGCPADEREF) statistics | ||
| Number of states | 1 | |
| Total time for successor computation | 0.010s | |
| Total time for strengthen operator | 0.129s | |
| Automaton transfers with branching | 0 | |
| Automaton transfer successors | 1.00 | sum: 231, count: 231, min: 1, max: 1 [1 x 231] |
| Number of states with assumption transitions | 0 | |
| AutomatonAnalysis (SMGCPAFREE) statistics | ||
| Number of states | 1 | |
| Total time for successor computation | 0.005s | |
| Total time for strengthen operator | 0.086s | |
| Automaton transfers with branching | 0 | |
| Automaton transfer successors | 1.00 | sum: 231, count: 231, min: 1, max: 1 [1 x 231] |
| Number of states with assumption transitions | 0 | |
| AutomatonAnalysis (SMGCPAMEMTRACK) statistics | ||
| Number of states | 1 | |
| Total time for successor computation | 0.002s | |
| Total time for strengthen operator | 0.074s | |
| Automaton transfers with branching | 0 | |
| Automaton transfer successors | 1.00 | sum: 231, count: 231, min: 1, max: 1 [1 x 231] |
| Number of states with assumption transitions | 0 | |
| AutomatonAnalysis (svcompTerminatingFunctions) statistics | ||
| Number of states | 1 | |
| Total time for successor computation | 0.016s | |
| Automaton transfers with branching | 0 | |
| Automaton transfer successors | 1.00 | sum: 231, count: 231, min: 1, max: 1 [1 x 231] |
| Number of states with assumption transitions | 0 | |
| CPA algorithm statistics | ||
| Number of iterations | 31 | |
| Max size of waitlist | 5 | |
| Average size of waitlist | 2 | |
| Number of computed successors | 35 | |
| Max successors for one state | 2 | |
| Number of times merged | 0 | |
| Number of times stopped | 1 | |
| Number of times breaked | 1 | |
| Total time for CPA algorithm | 1.256s | Max: 1.256s |
| Time for choose from waitlist | 0.001s | |
| Time for precision adjustment | 0.042s | |
| Time for transfer relation | 1.174s | |
| Time for stop operator | 0.037s | |
| Time for adding to reached set | 0.000s | |
| Statistics for | /opt/cpachecker/config/components/smgAnalysis-symEx-concrete-memory-access.properties | |
| ===================================================================================================== | ||
| Time spent in analysis thread /opt/cpachecker/config/components/smgAnalysis-symEx-concrete-memory-access.properties | 0.002s | |
| SMGCPA statistics | ||
| Number of variables per state | 15.55 | sum: 342, count: 22, min: 0, max: 20 |
| Number of global variables per state | 8.14 | sum: 179, count: 22, min: 0, max: 9 |
| Time for solving constraints | 0.285s | |
| Time for independent computation | 0.002s | |
| Time for SMT check | 0.006s | |
| Time for resolving definites | 0.046s | |
| Cache lookups | 9 | |
| Direct cache hits | 1 | |
| Direct cache lookup time | 0.000s | |
| Number of assumptions | 12 | |
| Number of deterministic assumptions | 0 | |
| Level of Determinism | 0% | |
| Number of list materializations | : 0 | |
| Total time spent on materialization | : 0ms | |
| Max time spent on materialization | : 0ms | |
| Number of 0+ materializations | 0 | |
| Total time spent on 0+ materialization | : 0ms | |
| Max time spent on 0+ materialization | : 0ms | |
| Number of lists abstracted in total | : 0 | |
| Total time spent on list abstraction | : 0ms | |
| Max time spent on list abstraction | : 0ms | |
| Total time spent on searching for list abstractions | : 0ms | |
| Max time spent on searching a single list abstractions | : 0ms | |
| AutomatonAnalysis (SMGCPADEREF) statistics | ||
| Number of states | 1 | |
| Total time for successor computation | 0.029s | |
| Total time for strengthen operator | 0.146s | |
| Automaton transfers with branching | 0 | |
| Automaton transfer successors | 1.00 | sum: 215, count: 215, min: 1, max: 1 [1 x 215] |
| Number of states with assumption transitions | 0 | |
| AutomatonAnalysis (SMGCPAFREE) statistics | ||
| Number of states | 1 | |
| Total time for successor computation | 0.010s | |
| Total time for strengthen operator | 0.116s | |
| Automaton transfers with branching | 0 | |
| Automaton transfer successors | 1.00 | sum: 215, count: 215, min: 1, max: 1 [1 x 215] |
| Number of states with assumption transitions | 0 | |
| AutomatonAnalysis (SMGCPAMEMTRACK) statistics | ||
| Number of states | 1 | |
| Total time for successor computation | 0.004s | |
| Total time for strengthen operator | 0.139s | |
| Automaton transfers with branching | 0 | |
| Automaton transfer successors | 1.00 | sum: 215, count: 215, min: 1, max: 1 [1 x 215] |
| Number of states with assumption transitions | 0 | |
| AutomatonAnalysis (svcompTerminatingFunctions) statistics | ||
| Number of states | 1 | |
| Total time for successor computation | 0.008s | |
| Automaton transfers with branching | 0 | |
| Automaton transfer successors | 1.00 | sum: 215, count: 215, min: 1, max: 1 [1 x 215] |
| Number of states with assumption transitions | 0 | |
| CPA algorithm statistics | ||
| Number of iterations | 18 | |
| Max size of waitlist | 5 | |
| Average size of waitlist | 1 | |
| Number of computed successors | 21 | |
| Max successors for one state | 2 | |
| Number of times merged | 0 | |
| Number of times stopped | 0 | |
| Number of times breaked | 0 | |
| Total time for CPA algorithm | 1.196s | Max: 1.196s |
| Time for choose from waitlist | 0.000s | |
| Time for precision adjustment | 0.072s | |
| Time for transfer relation | 1.113s | |
| Time for stop operator | 0.009s | |
| Time for adding to reached set | 0.000s | |
| Statistics for | /opt/cpachecker/config/components/smgValueAnalysis-abstract-concrete-values-with-cex.properties | |
| =============================================================================================================== | ||
| Time spent in analysis thread /opt/cpachecker/config/components/smgValueAnalysis-abstract-concrete-values-with-cex.properties | 0.429s | |
| SMGCPA statistics | ||
| Number of variables per state | 17.36 | sum: 573, count: 33, min: 0, max: 25 |
| Number of global variables per state | 8.48 | sum: 280, count: 33, min: 0, max: 10 |
| Number of assumptions | 16 | |
| Number of deterministic assumptions | 0 | |
| Level of Determinism | 0% | |
| Number of list materializations | : 0 | |
| Total time spent on materialization | : 0ms | |
| Max time spent on materialization | : 0ms | |
| Number of 0+ materializations | 0 | |
| Total time spent on 0+ materialization | : 0ms | |
| Max time spent on 0+ materialization | : 0ms | |
| Number of lists abstracted in total | : 0 | |
| Total time spent on list abstraction | : 0ms | |
| Max time spent on list abstraction | : 0ms | |
| Total time spent on searching for list abstractions | : 0ms | |
| Max time spent on searching a single list abstractions | : 0ms | |
| AutomatonAnalysis (SMGCPADEREF) statistics | ||
| Number of states | 1 | |
| Total time for successor computation | 0.028s | |
| Total time for strengthen operator | 0.210s | |
| Automaton transfers with branching | 0 | |
| Automaton transfer successors | 1.00 | sum: 230, count: 230, min: 1, max: 1 [1 x 230] |
| Number of states with assumption transitions | 0 | |
| AutomatonAnalysis (SMGCPAFREE) statistics | ||
| Number of states | 1 | |
| Total time for successor computation | 0.025s | |
| Total time for strengthen operator | 0.116s | |
| Automaton transfers with branching | 0 | |
| Automaton transfer successors | 1.00 | sum: 230, count: 230, min: 1, max: 1 [1 x 230] |
| Number of states with assumption transitions | 0 | |
| AutomatonAnalysis (SMGCPAMEMTRACK) statistics | ||
| Number of states | 1 | |
| Total time for successor computation | 0.005s | |
| Total time for strengthen operator | 0.055s | |
| Automaton transfers with branching | 0 | |
| Automaton transfer successors | 1.00 | sum: 230, count: 230, min: 1, max: 1 [1 x 230] |
| Number of states with assumption transitions | 0 | |
| AutomatonAnalysis (svcompTerminatingFunctions) statistics | ||
| Number of states | 1 | |
| Total time for successor computation | 0.007s | |
| Automaton transfers with branching | 0 | |
| Automaton transfer successors | 1.00 | sum: 230, count: 230, min: 1, max: 1 [1 x 230] |
| Number of states with assumption transitions | 0 | |
| CPA algorithm statistics | ||
| Number of iterations | 28 | |
| Max size of waitlist | 5 | |
| Average size of waitlist | 2 | |
| Number of computed successors | 34 | |
| Max successors for one state | 2 | |
| Number of times merged | 0 | |
| Number of times stopped | 2 | |
| Number of times breaked | 1 | |
| Total time for CPA algorithm | 0.913s | Max: 0.913s |
| Time for choose from waitlist | 0.000s | |
| Time for precision adjustment | 0.064s | |
| Time for transfer relation | 0.776s | |
| Time for stop operator | 0.057s | |
| Time for adding to reached set | 0.008s | |
| Counterexample-Check Algorithm statistics | ||
| Number of counterexample checks | 1 | |
| Number of infeasible paths | 0 | 0% |
| Time for counterexample checks | 1.642s | |
| Statistics for | /opt/cpachecker/config/components/smgValueAnalysis-with-cex.properties | |
| ====================================================================================== | ||
| Time spent in analysis thread /opt/cpachecker/config/components/smgValueAnalysis-with-cex.properties | 0.432s | |
| SMGCPA statistics | ||
| Number of variables per state | 19.05 | sum: 819, count: 43, min: 0, max: 28 |
| Number of global variables per state | 8.74 | sum: 376, count: 43, min: 0, max: 10 |
| Number of assumptions | 24 | |
| Number of deterministic assumptions | 0 | |
| Level of Determinism | 0% | |
| Number of list materializations | : 0 | |
| Total time spent on materialization | : 0ms | |
| Max time spent on materialization | : 0ms | |
| Number of 0+ materializations | 0 | |
| Total time spent on 0+ materialization | : 0ms | |
| Max time spent on 0+ materialization | : 0ms | |
| Number of lists abstracted in total | : 0 | |
| Total time spent on list abstraction | : 0ms | |
| Max time spent on list abstraction | : 0ms | |
| Total time spent on searching for list abstractions | : 0ms | |
| Max time spent on searching a single list abstractions | : 0ms | |
| AutomatonAnalysis (SMGCPADEREF) statistics | ||
| Number of states | 1 | |
| Total time for successor computation | 0.024s | |
| Total time for strengthen operator | 0.192s | |
| Automaton transfers with branching | 0 | |
| Automaton transfer successors | 1.00 | sum: 244, count: 244, min: 1, max: 1 [1 x 244] |
| Number of states with assumption transitions | 0 | |
| AutomatonAnalysis (SMGCPAFREE) statistics | ||
| Number of states | 1 | |
| Total time for successor computation | 0.003s | |
| Total time for strengthen operator | 0.169s | |
| Automaton transfers with branching | 0 | |
| Automaton transfer successors | 1.00 | sum: 244, count: 244, min: 1, max: 1 [1 x 244] |
| Number of states with assumption transitions | 0 | |
| AutomatonAnalysis (SMGCPAMEMTRACK) statistics | ||
| Number of states | 1 | |
| Total time for successor computation | 0.011s | |
| Total time for strengthen operator | 0.082s | |
| Automaton transfers with branching | 0 | |
| Automaton transfer successors | 1.00 | sum: 244, count: 244, min: 1, max: 1 [1 x 244] |
| Number of states with assumption transitions | 0 | |
| AutomatonAnalysis (svcompTerminatingFunctions) statistics | ||
| Number of states | 1 | |
| Total time for successor computation | 0.004s | |
| Automaton transfers with branching | 0 | |
| Automaton transfer successors | 1.00 | sum: 244, count: 244, min: 1, max: 1 [1 x 244] |
| Number of states with assumption transitions | 0 | |
| CPA algorithm statistics | ||
| Number of iterations | 38 | |
| Max size of waitlist | 5 | |
| Average size of waitlist | 2 | |
| Number of computed successors | 44 | |
| Max successors for one state | 2 | |
| Number of times merged | 0 | |
| Number of times stopped | 2 | |
| Number of times breaked | 1 | |
| Total time for CPA algorithm | 0.964s | Max: 0.964s |
| Time for choose from waitlist | 0.001s | |
| Time for precision adjustment | 0.070s | |
| Time for transfer relation | 0.787s | |
| Time for stop operator | 0.087s | |
| Time for adding to reached set | 0.003s | |
| Counterexample-Check Algorithm statistics | ||
| Number of counterexample checks | 1 | |
| Number of infeasible paths | 0 | 0% |
| Time for counterexample checks | 1.583s | |
| Statistics for | /opt/cpachecker/config/components/smgAnalysis-symEx-overapproximating-with-cex.properties | |
| ========================================================================================================= | ||
| Time spent in analysis thread /opt/cpachecker/config/components/smgAnalysis-symEx-overapproximating-with-cex.properties | 0.304s | |
| SMGCPA statistics | ||
| Number of variables per state | 15.74 | sum: 362, count: 23, min: 0, max: 20 |
| Number of global variables per state | 8.17 | sum: 188, count: 23, min: 0, max: 9 |
| Time for solving constraints | 0.245s | |
| Time for independent computation | 0.009s | |
| Time for SMT check | 0.029s | |
| Time for resolving definites | 0.066s | |
| Cache lookups | 9 | |
| Direct cache hits | 0 | |
| Direct cache lookup time | 0.000s | |
| Number of assumptions | 12 | |
| Number of deterministic assumptions | 0 | |
| Level of Determinism | 0% | |
| Number of list materializations | : 0 | |
| Total time spent on materialization | : 0ms | |
| Max time spent on materialization | : 0ms | |
| Number of 0+ materializations | 0 | |
| Total time spent on 0+ materialization | : 0ms | |
| Max time spent on 0+ materialization | : 0ms | |
| Number of lists abstracted in total | : 0 | |
| Total time spent on list abstraction | : 0ms | |
| Max time spent on list abstraction | : 0ms | |
| Total time spent on searching for list abstractions | : 0ms | |
| Max time spent on searching a single list abstractions | : 0ms | |
| AutomatonAnalysis (SMGCPADEREF) statistics | ||
| Number of states | 1 | |
| Total time for successor computation | 0.012s | |
| Total time for strengthen operator | 0.304s | |
| Automaton transfers with branching | 0 | |
| Automaton transfer successors | 1.00 | sum: 216, count: 216, min: 1, max: 1 [1 x 216] |
| Number of states with assumption transitions | 0 | |
| AutomatonAnalysis (SMGCPAFREE) statistics | ||
| Number of states | 1 | |
| Total time for successor computation | 0.000s | |
| Total time for strengthen operator | 0.198s | |
| Automaton transfers with branching | 0 | |
| Automaton transfer successors | 1.00 | sum: 216, count: 216, min: 1, max: 1 [1 x 216] |
| Number of states with assumption transitions | 0 | |
| AutomatonAnalysis (SMGCPAMEMTRACK) statistics | ||
| Number of states | 1 | |
| Total time for successor computation | 0.002s | |
| Total time for strengthen operator | 0.119s | |
| Automaton transfers with branching | 0 | |
| Automaton transfer successors | 1.00 | sum: 216, count: 216, min: 1, max: 1 [1 x 216] |
| Number of states with assumption transitions | 0 | |
| AutomatonAnalysis (svcompTerminatingFunctions) statistics | ||
| Number of states | 1 | |
| Total time for successor computation | 0.001s | |
| Automaton transfers with branching | 0 | |
| Automaton transfer successors | 1.00 | sum: 216, count: 216, min: 1, max: 1 [1 x 216] |
| Number of states with assumption transitions | 0 | |
| CPA algorithm statistics | ||
| Number of iterations | 18 | |
| Max size of waitlist | 5 | |
| Average size of waitlist | 1 | |
| Number of computed successors | 22 | |
| Max successors for one state | 2 | |
| Number of times merged | 0 | |
| Number of times stopped | 0 | |
| Number of times breaked | 1 | |
| Total time for CPA algorithm | 1.275s | Max: 1.275s |
| Time for choose from waitlist | 0.001s | |
| Time for precision adjustment | 0.049s | |
| Time for transfer relation | 1.195s | |
| Time for stop operator | 0.014s | |
| Time for adding to reached set | 0.002s | |
| Counterexample-Check Algorithm statistics | ||
| Number of counterexample checks | 1 | |
| Number of infeasible paths | 0 | 0% |
| Time for counterexample checks | 1.272s | |
| Other statistics | ||
| ================ | ||
| Code Coverage | ||
| Function coverage | 0.050 | |
| Visited lines | 134 | |
| Total lines | 507 | |
| Line coverage | 0.264 | |
| Visited conditions | 11 | |
| Total conditions | 66 | |
| Condition coverage | 0.167 | |
| CPAchecker general statistics | ||
| Number of program locations | 778 | |
| Number of CFA edges (per node) | 765 | count: 778, min: 0, max: 8, avg: 0.98 |
| Number of relevant variables | 111 | |
| Number of functions | 80 | |
| Number of loops (and loop nodes) | 6 | sum: 52, min: 5, max: 14, avg: 8.67 |
| Size of reached set | 35 | |
| Number of reached locations | 30 | 4% |
| Avg states per location | 1 | |
| Max states per location | 4 | at node N378 |
| Number of reached functions | 4 | 5% |
| Number of partitions | 30 | |
| Avg size of partitions | 1 | |
| Max size of partitions | 4 | with key [N378 before line 961, Function CWE789_Uncontrolled_Mem_Alloc__malloc_char_connect_socket_01_bad called from node N406, stack depth 2 [73fafd4], stack [main, CWE789_Uncontrolled_Mem_Alloc__malloc_char_connect_socket_01_bad], 20] |
| Number of target states | 1 | |
| Size of final wait list | 4 | |
| Time for analysis setup | 7.745s | |
| Time for loading CPAs | 2.632s | |
| Time for loading parser | 0.569s | |
| Time for CFA construction | 3.404s | |
| Time for parsing file(s) | 0.773s | |
| Time for AST to CFA | 0.970s | |
| Time for CFA sanity check | 0.148s | |
| Time for post-processing | 1.384s | |
| Time for loop structure | 0.039s | |
| Time for AST structure | 0.000s | |
| Time for CFA export | 2.156s | |
| Time for function pointers resolving | 0.021s | |
| Function calls via function pointers | 1 | count: 1, min: 1, max: 1, avg: 1.00 |
| Instrumented function pointer calls | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Function calls with function pointer arguments | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Instrumented function pointer arguments | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Time for classifying variables | 0.416s | |
| Time for collecting variables | 0.250s | |
| Time for solving dependencies | 0.008s | |
| Time for building hierarchy | 0.000s | |
| Time for building classification | 0.095s | |
| Time for exporting data | 0.063s | |
| Time for Analysis | 2.661s | |
| CPU time for analysis | 7.500s | |
| Time for analyzing result | 0.002s | |
| Total time for CPAchecker | 10.409s | |
| Total CPU time for CPAchecker | 21.010s | |
| Time for statistics | 0.215s | |
| Time for Garbage Collector | 0.562s | in 4 runs |
| Garbage Collector(s) used | PS MarkSweep, PS Scavenge | |
| Used heap memory | 191MB ( 182 MiB) max; 98MB ( 94 MiB) avg; 211MB ( 201 MiB) peak | |
| Used non-heap memory | 54MB ( 52 MiB) max; 36MB ( 34 MiB) avg; 56MB ( 53 MiB) peak | |
| Used in PS Old Gen pool | 20MB ( 19 MiB) max; 9MB ( 8 MiB) avg; 20MB ( 19 MiB) peak | |
| Allocated heap memory | 1002MB ( 956 MiB) max; 1002MB ( 956 MiB) avg | |
| Allocated non-heap memory | 57MB ( 55 MiB) max; 38MB ( 37 MiB) avg | |
| Total process virtual memory | 5609MB ( 5350 MiB) max; 4716MB ( 4498 MiB) avg |
| # | Configuration Name | Configuration Value |
|---|---|---|
| 1 | analysis.entryFunction | main |
| 2 | analysis.programNames | CWE789-1/CWE789_Uncontrolled_Mem_Alloc---s01---CWE789_Uncontrolled_Mem_Alloc__malloc_char_connect_socket_01_bad.i |
| 3 | analysis.useParallelAnalyses | true |
| 4 | cfa.findLiveVariables | true |
| 5 | cfa.simplifyCfa | false |
| 6 | counterexample.export.compressWitness | false |
| 7 | counterexample.export.graphml | witness.graphml |
| 8 | counterexample.export.yaml | witness.yml |
| 9 | cpa.arg.compressWitness | false |
| 10 | cpa.arg.yamlProofWitness | witness.yml |
| 11 | cpa.callstack.unsupportedFunctions | pthread_create,pthread_key_create,sin,cos,__builtin_uaddl_overflow,_longjmp,longjmp,siglongjmp |
| 12 | cpa.smg2.handleUnknownFunctions | ASSUME_EXTERNAL_ALLOCATED |
| 13 | language | C |
| 14 | limits.time.cpu | 30 |
| 15 | parallelAlgorithm.configFiles | smgAnalysis-symEx.properties, smgAnalysis-symEx-concrete-memory-access.properties, smgValueAnalysis-abstract-concrete-values-with-cex.properties, smgValueAnalysis-with-cex.properties, smgAnalysis-symEx-overapproximating-with-cex.properties |
| 16 | specification | properties/valid-memsafety.prp |
This table was generated by CPAchecker. For feedback, questions, and bug reports please use our issue tracker.
License: Apache 2.0 License
Source: {{dependency.repository}}
{{dependency.copyright}}
License:
Full text of license
{{dependencies.licenses[dependency.licenseId]}}